Nuprl Lemma : add_functionality_wrt_eq
12,41
postcript
pdf
i1
,
i2
,
j1
,
j2
:
. (
i1
=
j1
)
(
i2
=
j2
)
(
i1
+
i2
=
j1
+
j2
)
latex
ProofTree
Definitions
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
origin
i1, i2, j1, j2:
. (i1 = j1) 
(i2 = j2) (i1+i2 = j1+j2)
i1, i2, j1, j2:. (i1 = j1) (i2 = j2) (i1+i2 = j1+j2)
T Qx:A. B(x)